In the course of designing a new computer application or operating system, typically one first writes a program specification for the application. Authoring of the program specification includes specifying the functions the application or system will have to fulfill, defining the types and uses of variables, defining parameters and their relationships, and the other requirements which go into a conventional program specification.
Such a program specification may be quite extensive. For instance, for the widespread version of UNIX known as POSIX, the specification for the system application program interface (API) for the C programming language runs over 350 pages in the book entitled ISO/IEC 9945-1 (IEEE Std 1003.1)/Information Technology-Portable Operating System Interface (POSIX)-Part I (First Edition 1990-12-07), which is incorporated herein by reference.
Software application developers, system engineers, end users operating in a UNIX environment and others refer to such a specification whenever they author applications based upon it. Typically, such applications are tested during and after their creation, for internal consistency and to ensure that they perform as intended. Such testing will be referred to herein as validation testing.
In the case of POSIX, for example, the above-mentioned IEEE reference provides the complete English-language specification of POSIX for the C programming language. Whenever a programmer writes an application in C to run on the POSIX operating system, this reference must be consulted to ensure that all of the standards are being complied with.
It is a very difficult and involved matter to ensure that an implementation of a long program specification is consistent with the specification of POSIX, and yet this is crucial for the proper operation of the implementation and anything based upon it. Testing and verifying the implementation is particularly important when the program specification is for a computer language such as C or an operating system such as UNIX. If, for instance, an operating system based upon POSIX includes errors, those errors will create bugs in all programs that run on the erroneous operating system. Thus, before the implementation of POSIX is ever released, it should be fully tested.
Such an implementation will, for the POSIX 1003.1 specification mentioned above, take the form of a program written in the C language. Thus, the validation tests to be run must verify the correctness of this C implementation of the program specification.
The concept of specification testing is represented, for example, by STATEMATE, which provides a system by which a programmer can model a specification and test it. See The STATEMATE Approach to Complex Systems, by i-Logix of Burlington, Mass. (1990); and D. Harel et al., STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, Vol. 16, No. (April 1990). Testing the implementation of a specification (i.e. an application based on the specification), based upon traversal of a graph model based upon the implementation, is discussed in W. H. Jessop et al., Atlas-An Automated Software Testing System, Bell Laboratories, Inc., 13th IEEE Computer Society International Conference, pp. 337-340 (1976) and 2nd International Conference on Software Engineering, pp. 629-635 (1976). Various test selection methods for systems expressed as finite state machines are discussed in S. Fujiwara et al., Test Selection Based on Finite State Models, IEEE Transactions on Software Engineering, Vol. 17, No. 6 (June 1991) and W. H. Jessop et al. Each of the foregoing articles is incorporated herein by reference.
With the STATEMATE system, the user must convert the English-language (as opposed to computer code) program specification into a machine-readable coding. Neither STATEMATE nor other prior systems automatically generate validation tests for the actual implementation of the program specification, i.e. for applications with which they are designed to comply.
To generate validation tests of an application, the systems described in the Jessop and Fujiwara articles rely upon an expression of the program specification as a finite state machine (FSM). Essentially any program specification or software application can theoretically be expressed as an FSM, whether the modeled entity is state-rich or expressed as data relationships. An "extended" finite state machine adds context to the transitions (i.e. a record of the history of traversal of the transitions). See the Introduction below for a formal definition of EFSM.
FSMs and EFSMs are particularly suited to state-rich problems. A program is state-rich if it controls a system where the state of the system at any given time is important, such as a program to control an automatic teller machine. A program specification for an operating system interface or a program routine, on the other hand, is typically data-rich; that is, the specification is described largely in terms of detailed data structures and their relationships.
Although one can, if necessary, generate an FSM to represent a data-rich program specification as states with transitions from one state to another, such a model does not serve well as a human-readable program specification.
In addition, hand-generated graph models are subject to the limitations of the programmer who creates them, which can lead to testing inefficiencies or inaccuracies, particularly in the case of a data-rich setting. Data-rich problems are particularly unsuited to being expressed as graph models such as FSMs, since they are by definition descriptions of data relationships, not of states and transitions. Thus, although a data-rich program specification can be expressed as an FSM, it is very cumbersome to do so, and is not an intuitive way to approach the problem. Moreover, while such a model would be computer-readable, it could not easily be interpreted by humans if complicated data structures are involved. For this reason, FSM-based Systems (such as Atlas) are not, in general, useful for data-rich problems. The cited articles do not teach any mechanism for automatically generating validation tests using the program specification itself as a starting point.
A system is needed which bypasses the necessity for human intervention in the creation of models to generate testing software against a program specification, and which at the same time an produce a set of tests which are accurate and which can be tailored to any degree of comprehensiveness, from testing all possible paths through the model to testing only few. In particular, a system is needed which allows for modeling of a program specification in a manner which is suitable for humans, but which leads directly to an expression of the model which can be used by a computer to generate validation tests for the implementation of the software.